c formula generated with seed 9, probabilty values 0.414000 0.028000 0.503000 and clause ration 4.408889
c the planted solution is {1, 3, 4, 5, 6, 7, 8, 9, 13, 14, 15, 19, 20, 22, 26, 28, 29, 30, 32, 36, 42, 46, 47, 48, 51, 54, 55, 56, 60, 61, 63, 64, 66, 68, 69, 71, 72, 74, 77, 78, 82, 87, 88, 89, 94, 97, 100, 101, 102, 103, 104, 107, 108, 110, 112, 116, 117, 118, 120, 122, 123, 124, 128, 130, 131, 135, 144, 145, 147, 148, 152, 154, 158, 159, 161, 162, 163, 164, 166, 167, 169, 170, 171, 173, 174, 175, 177, 178, 183, 185, 189, 194, 197, 199, 200, 202, 203, 204, 205, 206, 211, 213, 216, 217, 219, 225, 227, 230, 231, 234, 235, 236, 238, 240, 242, 244, 246, 247, 248, 250, 252, 253, 258, 260, 261, 262, 264, 268, 271, 272, 274, 278, 279, 282, 283, 284, 286, 288, 293, 296, 298, 300, 308, 309, 310, 311, 313, 315, 316, 317, 318, 319, 323, 324, 325, 326, 327, 328, 331, 335, 336, 337, 338, 340, 341, 345, 348, 349, 354, 355, 356, 357, 359, 361, 362, 364, 366, 367, 372, 373, 374, 377, 378, 379, 380, 389, 390, 394, 395, 398, 401, 403, 406, 407, 408, 411, 412, 413, 414, 415, 416, 417, 418, 421, 423, 424, 426, 427, 429, 431, 432, 435, 438, 440, 441, 444, 445, 446, 447, 448, 449, 450}
p cnf 450 1984
-132 87 -430 0
-88 427 -200 0
94 413 -294 0
-140 -321 411 0
-415 -335 -41 0
-143 -41 197 0
-145 -169 264 0
346 370 389 0
-9 -132 288 0
-35 342 52 0
-386 319 -151 0
-405 -242 346 0
-46 -338 -265 0
65 -74 252 0
-213 -242 -369 0
23 268 251 0
39 420 -388 0
150 -121 276 0
344 359 -47 0
-363 291 -74 0
-54 -404 332 0
-4 449 -97 0
308 -105 -228 0
330 -207 165 0
236 223 224 0
74 -149 -95 0
284 200 264 0
286 -168 -276 0
88 90 388 0
-352 36 -149 0
-207 234 -76 0
-416 -69 318 0
-236 -332 392 0
103 57 142 0
139 -239 40 0
219 360 226 0
-71 -63 -391 0
-398 -352 370 0
427 196 407 0
313 329 119 0
349 -147 80 0
211 -49 -155 0
-239 -179 56 0
-414 52 311 0
-312 -393 -290 0
-251 360 -261 0
-89 345 -123 0
-408 338 -283 0
312 257 -192 0
313 207 297 0
107 -305 -198 0
-78 -324 -119 0
-418 -292 -128 0
-94 197 -288 0
377 -381 -269 0
-321 -409 -97 0
-317 316 215 0
371 -162 46 0
19 409 -117 0
-360 -399 55 0
-357 -68 122 0
-253 314 -33 0
-88 426 -264 0
-15 243 -114 0
-89 441 -47 0
-354 -360 -183 0
-95 82 -212 0
-188 -311 156 0
-414 -285 -408 0
395 -273 -314 0
-48 322 55 0
-342 188 154 0
283 -221 -198 0
-145 -106 439 0
120 243 -424 0
-40 93 333 0
402 415 304 0
146 -394 -265 0
-110 -355 -153 0
343 398 -4 0
125 290 440 0
279 430 113 0
411 112 -237 0
-112 -156 -123 0
141 -411 -292 0
295 287 13 0
-395 -39 215 0
70 -239 -89 0
-267 279 -290 0
61 95 -26 0
-177 409 355 0
150 439 338 0
-265 142 109 0
162 408 42 0
-276 -410 -139 0
-189 -410 -66 0
91 -321 351 0
-352 -76 -304 0
188 -352 58 0
-428 74 174 0
-401 -356 -146 0
158 429 163 0
66 -145 -108 0
-116 264 -46 0
-129 425 39 0
-384 -16 -399 0
-250 -145 390 0
-396 30 -105 0
289 -392 259 0
54 -51 -407 0
-2 -426 260 0
396 -256 249 0
1 -235 151 0
429 286 398 0
70 313 297 0
-424 186 445 0
-285 423 -437 0
-155 39 -78 0
-214 -340 -130 0
404 83 56 0
335 -350 -109 0
394 -87 -367 0
-139 53 -144 0
-400 112 147 0
-307 71 66 0
-446 93 -370 0
183 262 -92 0
-220 -145 96 0
-182 395 -404 0
242 -65 -186 0
-398 59 71 0
-108 -254 121 0
-126 112 288 0
157 95 230 0
20 341 28 0
-187 -251 206 0
327 -363 -156 0
-151 -223 417 0
-278 -390 -228 0
-441 429 179 0
15 -12 -239 0
424 322 265 0
142 5 -235 0
-106 104 199 0
261 375 -139 0
142 346 -243 0
-151 -262 251 0
186 76 -232 0
426 -204 -447 0
278 384 201 0
73 -209 343 0
-45 -322 -383 0
133 170 -47 0
-351 -34 -142 0
-185 59 445 0
210 132 253 0
-243 -368 279 0
116 -143 380 0
-177 -440 183 0
1 -191 28 0
-159 -437 -298 0
304 -155 -380 0
167 -223 444 0
-48 59 235 0
-294 3 305 0
-130 51 -202 0
-40 444 -190 0
88 -181 -34 0
-195 364 338 0
320 358 78 0
-345 -367 -302 0
102 11 283 0
-158 -38 -371 0
-244 330 260 0
-304 298 -165 0
-53 324 -434 0
134 -301 -412 0
-135 136 -280 0
304 251 -433 0
335 153 -416 0
-430 267 137 0
-157 218 -264 0
-382 356 154 0
333 -157 18 0
406 107 380 0
-242 -130 -383 0
307 362 92 0
440 -315 337 0
-324 343 -404 0
-311 -285 307 0
-356 376 377 0
106 -23 154 0
167 59 -231 0
426 -440 -389 0
4 142 -286 0
-145 -214 371 0
290 -209 360 0
216 247 -409 0
116 -113 135 0
53 371 -322 0
-303 81 233 0
103 -15 232 0
104 26 309 0
13 424 247 0
30 148 -311 0
333 -359 244 0
288 -25 -358 0
301 374 265 0
119 176 286 0
94 -446 225 0
-261 -155 -390 0
-29 236 -87 0
217 -245 -17 0
-333 390 170 0
448 -7 -311 0
-406 186 -436 0
-432 -376 351 0
-254 -289 -256 0
-389 341 405 0
-102 402 171 0
-286 -118 373 0
331 375 -56 0
-203 57 -16 0
329 379 96 0
-411 129 -191 0
-22 -46 -368 0
-11 374 -126 0
241 -356 -391 0
358 -401 427 0
143 207 240 0
438 -271 -250 0
-382 308 -383 0
-42 -10 23 0
-262 -9 -419 0
269 -354 -142 0
-116 -341 262 0
-442 -385 -419 0
-309 58 87 0
173 -411 -348 0
-43 -111 -233 0
397 276 407 0
29 -114 -184 0
214 40 -129 0
40 142 144 0
93 38 88 0
-207 -100 -341 0
-388 259 -330 0
-93 182 -264 0
318 292 333 0
-278 -210 -407 0
69 -393 -18 0
286 -304 -142 0
434 -91 -450 0
-165 -41 -84 0
269 42 290 0
79 -435 -50 0
244 39 370 0
42 90 -335 0
41 -206 238 0
-3 -174 418 0
229 385 -106 0
180 24 199 0
-113 -204 124 0
-213 243 -269 0
435 294 -124 0
-300 448 289 0
-170 -112 -192 0
290 273 -86 0
300 9 -186 0
437 190 -151 0
-113 -294 194 0
-318 -239 -120 0
-93 250 -410 0
-49 238 71 0
183 174 147 0
-286 305 -393 0
-444 -148 -86 0
359 115 210 0
8 -390 -305 0
-272 259 -111 0
-217 -62 -203 0
-418 -263 11 0
78 447 -255 0
205 -204 193 0
-299 -131 -240 0
-171 -297 -178 0
128 380 28 0
-119 -373 106 0
288 -348 -286 0
-226 49 -311 0
-425 355 -133 0
-125 175 -119 0
-321 -328 212 0
-258 -73 181 0
-361 -206 -181 0
413 403 110 0
227 413 -83 0
-101 305 19 0
-311 255 424 0
-13 -449 -11 0
404 430 -143 0
-347 441 414 0
296 403 -65 0
423 -434 120 0
-58 83 -379 0
159 -63 134 0
-360 -130 -274 0
169 -402 -153 0
153 -179 -61 0
-50 338 284 0
96 -442 363 0
156 80 -57 0
-39 -144 371 0
353 28 79 0
172 147 -362 0
97 -21 -270 0
-61 -15 323 0
-110 -244 -281 0
16 -269 -161 0
-84 -79 -304 0
-127 -345 11 0
260 111 338 0
184 -40 277 0
394 -371 169 0
340 -279 -27 0
-374 -315 124 0
208 155 144 0
-210 -135 386 0
449 114 -166 0
152 412 406 0
-159 -187 -354 0
-127 -72 320 0
-136 -6 169 0
-110 176 28 0
-391 180 -123 0
-320 -50 128 0
-321 -242 -401 0
-28 101 239 0
195 -314 376 0
345 284 -342 0
113 -385 -316 0
-114 315 87 0
218 57 438 0
-121 -4 156 0
-177 -265 -283 0
152 -371 311 0
315 -410 288 0
85 -138 402 0
253 -105 -156 0
-436 -422 -295 0
375 -391 -189 0
-78 305 324 0
-99 -241 -228 0
68 -388 310 0
387 425 -267 0
37 88 44 0
364 -70 -95 0
341 -367 -22 0
209 102 -79 0
-247 396 -443 0
337 199 131 0
404 -330 433 0
182 -447 170 0
35 -41 307 0
297 158 24 0
-396 -430 -358 0
229 -208 52 0
-256 308 13 0
-150 -238 428 0
-208 -149 -113 0
361 222 -282 0
-367 228 -365 0
65 325 301 0
335 322 153 0
234 -328 188 0
437 -199 -322 0
-20 238 -354 0
-343 -197 -282 0
-417 -386 -248 0
198 -419 -364 0
-222 348 -280 0
-217 170 375 0
398 15 -83 0
-290 3 -292 0
438 39 307 0
361 -186 249 0
115 -116 -228 0
340 106 -308 0
-420 -78 -244 0
383 203 353 0
-285 78 -422 0
115 -259 136 0
342 -380 -430 0
-320 -72 -204 0
-189 -13 -405 0
79 -74 -119 0
172 449 62 0
-345 -240 261 0
1 389 315 0
301 213 381 0
-256 242 -360 0
-391 164 -367 0
-249 348 238 0
43 430 230 0
190 16 416 0
375 -437 -340 0
-277 -250 66 0
187 57 315 0
-186 -10 255 0
251 -370 -315 0
-120 -430 -48 0
-191 150 224 0
-296 293 17 0
-92 384 41 0
-372 423 -203 0
324 151 -122 0
289 -165 -72 0
34 207 -37 0
-357 -81 34 0
-42 -299 -247 0
-76 343 -94 0
-131 424 218 0
-362 -181 386 0
-332 226 53 0
-219 -129 297 0
412 -37 -138 0
-301 294 360 0
-252 -177 -232 0
-256 450 -126 0
-372 94 396 0
-282 393 145 0
193 153 213 0
-272 -12 363 0
-300 152 221 0
297 188 -196 0
194 -53 -44 0
-2 83 -240 0
-327 -375 138 0
410 -248 183 0
-181 -449 -413 0
-18 218 -449 0
-441 -334 -427 0
-85 -38 235 0
-340 -52 -77 0
-365 -194 -318 0
-385 193 425 0
195 -176 353 0
-299 -134 -369 0
422 -227 -215 0
-11 -350 -237 0
211 -3 -296 0
-144 -323 389 0
-278 177 157 0
82 -139 288 0
-81 -306 -192 0
395 149 -449 0
279 21 353 0
-363 -202 -335 0
-340 -388 192 0
-203 47 -116 0
-342 42 144 0
110 323 112 0
-254 363 49 0
293 -310 168 0
409 -164 -410 0
-250 -367 87 0
-298 -101 7 0
10 -210 -154 0
-389 315 -401 0
-97 -332 59 0
232 173 -167 0
197 -407 -415 0
85 406 40 0
-57 274 271 0
18 -10 146 0
-238 -375 304 0
239 -8 -149 0
-429 -79 297 0
81 311 84 0
-170 -354 94 0
64 11 334 0
276 12 -143 0
-424 122 -66 0
-103 -358 -444 0
-371 323 194 0
-366 194 -71 0
-310 252 -88 0
397 99 -267 0
-252 95 -44 0
415 213 -420 0
64 -196 175 0
-417 294 412 0
122 -165 -319 0
-270 -412 84 0
-178 434 278 0
45 -217 -422 0
346 -272 441 0
444 -113 123 0
111 -206 -392 0
30 -442 222 0
254 343 206 0
327 187 259 0
-378 342 -150 0
-19 -167 -196 0
-66 163 229 0
231 208 -445 0
-315 -310 1 0
-106 16 76 0
238 -392 -220 0
-91 -403 99 0
-224 -23 426 0
-168 -59 235 0
245 92 -62 0
-325 -148 429 0
-154 373 -323 0
440 -38 1 0
246 415 -443 0
-285 357 446 0
20 -408 -413 0
-386 -12 -11 0
317 65 128 0
432 -63 140 0
424 -82 -324 0
-216 31 272 0
333 -332 -167 0
-341 -368 312 0
264 2 270 0
375 -397 138 0
-373 340 -178 0
-130 -168 -87 0
63 -232 128 0
81 -423 -172 0
72 206 47 0
302 -243 -235 0
94 310 449 0
103 -334 175 0
-244 -365 10 0
421 -287 -263 0
75 27 403 0
407 153 -414 0
-442 -381 88 0
271 -37 -83 0
167 178 128 0
-403 116 -389 0
-141 186 -72 0
423 341 140 0
-227 415 91 0
-268 173 -7 0
112 448 240 0
33 -292 381 0
204 276 138 0
-187 303 -326 0
122 229 -345 0
25 379 84 0
-200 -419 -298 0
53 322 356 0
-263 86 332 0
28 77 -121 0
-210 -266 -306 0
-289 -370 -436 0
404 268 139 0
-439 -271 -3 0
-163 -132 11 0
-269 215 -194 0
-254 -149 367 0
165 -169 -16 0
279 -79 -265 0
296 216 227 0
83 228 -53 0
288 170 416 0
-251 -180 -45 0
294 48 -264 0
-149 -422 5 0
-396 173 135 0
60 -269 -263 0
-373 -417 -58 0
-221 -11 -109 0
257 -46 -98 0
428 64 -323 0
167 -317 -203 0
-319 407 -61 0
321 -256 -154 0
-40 -81 -39 0
306 -201 292 0
-64 2 308 0
80 -283 -65 0
9 315 -114 0
17 -24 114 0
-230 277 171 0
394 -23 -184 0
278 -396 338 0
410 -345 403 0
-194 -143 -424 0
-212 -427 -406 0
345 279 -350 0
-200 332 406 0
206 -240 62 0
67 425 -18 0
300 369 -203 0
440 79 -217 0
311 -360 167 0
155 390 404 0
11 -90 329 0
4 145 -306 0
254 -400 -225 0
292 -132 182 0
418 -235 180 0
-125 205 -103 0
-70 102 -106 0
264 374 60 0
21 -46 225 0
277 155 -301 0
-42 401 -367 0
122 -156 398 0
173 296 -43 0
122 413 128 0
349 275 -238 0
103 327 203 0
329 -107 -301 0
-302 -388 -127 0
-32 334 446 0
437 -140 -366 0
-101 200 289 0
414 293 -16 0
-336 -340 -50 0
253 243 179 0
96 -418 427 0
-97 16 3 0
-372 151 202 0
-114 426 -198 0
309 -394 -166 0
195 297 -65 0
397 -288 -334 0
422 290 311 0
85 -446 279 0
145 -104 -260 0
-435 370 -249 0
438 343 270 0
230 -86 -56 0
224 295 -33 0
106 -278 260 0
-318 -23 369 0
20 -197 -298 0
159 123 164 0
154 -201 44 0
77 -330 426 0
-60 96 -149 0
382 -12 121 0
-174 181 -212 0
-298 -132 -309 0
243 49 293 0
407 189 398 0
-98 306 -46 0
-287 -261 -147 0
328 -363 3 0
-31 399 137 0
-85 336 432 0
111 -278 -214 0
-273 353 -87 0
-51 -209 404 0
292 282 -357 0
171 -269 48 0
-212 74 -256 0
-84 -282 196 0
107 58 404 0
-78 -395 -57 0
-218 377 365 0
37 29 52 0
38 -60 -265 0
-168 -262 -124 0
-260 61 409 0
228 406 -71 0
418 36 -79 0
-205 -50 -108 0
202 383 32 0
-147 325 -277 0
296 410 269 0
195 -5 -111 0
-83 -186 -273 0
97 -264 -357 0
-390 161 306 0
369 -49 -185 0
-168 396 350 0
129 -138 167 0
315 83 -82 0
94 -340 434 0
-160 15 -380 0
-276 -21 218 0
-167 114 -419 0
-384 -117 -403 0
18 -98 -293 0
429 226 -13 0
-337 -56 247 0
-319 -183 -129 0
-179 78 28 0
-402 374 166 0
317 334 -205 0
-134 -293 -364 0
336 418 -369 0
-448 36 50 0
368 400 -53 0
-398 269 63 0
-262 208 173 0
431 212 -311 0
-188 -24 357 0
344 109 378 0
-106 -400 118 0
-114 -282 67 0
-35 328 -351 0
-92 -307 -49 0
63 -393 286 0
432 -443 204 0
325 447 240 0
181 -193 257 0
335 122 -184 0
87 -347 308 0
403 -8 -328 0
-167 223 -339 0
205 -95 -210 0
189 -372 -373 0
124 28 414 0
-88 439 -330 0
-406 -296 173 0
385 -352 -230 0
-7 258 -444 0
268 115 76 0
-364 -121 289 0
-260 345 -189 0
-253 354 92 0
28 -233 225 0
424 -256 279 0
-16 254 53 0
-225 163 -374 0
-328 -260 -209 0
301 -399 -124 0
271 -210 -285 0
-367 421 198 0
161 191 150 0
8 393 -414 0
158 -323 243 0
268 -135 -164 0
-189 327 -89 0
-292 -313 -189 0
266 126 -249 0
431 263 336 0
-443 -424 -390 0
-422 -329 200 0
183 404 67 0
368 128 215 0
113 -296 -95 0
438 -208 -190 0
354 -256 199 0
368 252 -14 0
-189 -228 -415 0
417 -284 399 0
-259 -196 -50 0
121 257 -127 0
150 -111 -78 0
-360 193 -216 0
220 -392 17 0
201 25 -285 0
360 -347 -102 0
441 -334 412 0
-152 -40 -440 0
-412 -186 58 0
120 -68 -197 0
389 277 156 0
-205 69 182 0
-64 -412 -140 0
-1 348 -372 0
-38 -358 -254 0
-18 -146 283 0
426 34 368 0
-42 442 123 0
9 300 -179 0
91 278 57 0
176 160 -132 0
367 224 -131 0
293 67 405 0
-209 286 315 0
153 399 418 0
-316 -435 242 0
406 -91 243 0
29 -423 -8 0
178 -334 -141 0
190 -337 331 0
22 -379 344 0
-231 340 -200 0
-98 -343 300 0
2 -74 -140 0
390 187 -124 0
230 225 -38 0
-419 174 -254 0
-90 81 -340 0
-259 358 396 0
139 183 360 0
151 -26 -287 0
-346 443 214 0
-327 169 44 0
447 -59 -259 0
-275 -429 -326 0
-123 -122 -232 0
-223 -352 161 0
306 -115 2 0
-231 -397 -107 0
-323 343 189 0
61 -39 -393 0
-185 106 -215 0
382 -294 18 0
-273 268 135 0
175 221 -77 0
85 -441 354 0
-447 -135 5 0
-390 21 341 0
-444 -351 156 0
-169 108 346 0
-124 -351 312 0
-251 331 -276 0
71 119 -373 0
290 -339 -429 0
-259 287 -406 0
319 298 359 0
-135 115 3 0
-209 -331 7 0
443 -90 -213 0
344 317 287 0
166 -180 423 0
-4 420 48 0
-117 442 319 0
448 180 160 0
383 327 221 0
174 -284 429 0
169 25 -445 0
4 -158 -315 0
142 -97 -223 0
275 293 -416 0
-47 423 -271 0
-271 293 98 0
-148 51 92 0
297 -414 318 0
12 -235 361 0
34 65 -351 0
-393 9 -52 0
-349 221 -273 0
-347 242 13 0
176 -113 -116 0
-5 -9 -333 0
302 202 -211 0
-6 -152 -179 0
131 366 -273 0
51 44 -66 0
268 -287 203 0
-433 396 -450 0
-13 120 18 0
44 -56 -111 0
-394 407 127 0
-274 -423 441 0
408 -321 300 0
40 56 17 0
427 -393 -369 0
-71 350 338 0
-294 380 200 0
133 -53 -371 0
-194 236 69 0
-431 64 -7 0
-426 -158 336 0
-399 140 -110 0
-225 -30 -410 0
333 -189 19 0
302 169 295 0
-267 28 9 0
-256 -428 52 0
418 -347 147 0
416 77 -314 0
-329 168 -429 0
-264 -369 15 0
369 -331 -287 0
238 -226 -353 0
-125 35 243 0
-350 -29 239 0
384 -353 75 0
432 448 -201 0
-226 -265 227 0
-234 -229 -135 0
76 443 -396 0
-78 379 70 0
-252 36 -389 0
-49 427 169 0
272 450 274 0
336 -83 279 0
-125 123 177 0
-388 246 449 0
-136 80 -260 0
-403 116 365 0
383 272 11 0
-428 -250 425 0
398 -146 -343 0
-344 -89 63 0
-247 169 -26 0
-150 105 -28 0
-288 -23 229 0
-292 97 200 0
353 -198 -284 0
41 -327 145 0
277 39 -314 0
-154 -10 -271 0
103 -327 263 0
-413 -181 2 0
-384 151 -120 0
305 -374 317 0
-242 198 -243 0
-263 225 -180 0
-305 -361 -245 0
-377 322 -31 0
-128 214 -386 0
-215 -342 -267 0
-355 -425 156 0
-236 -170 204 0
396 213 289 0
-304 91 -309 0
-285 391 103 0
34 -190 -15 0
254 -53 -250 0
285 44 324 0
83 230 -379 0
-248 152 190 0
263 -384 332 0
298 376 165 0
-200 -59 181 0
358 177 -101 0
-290 194 448 0
-370 198 226 0
422 32 290 0
-66 298 424 0
356 48 -428 0
-263 131 -208 0
-77 -17 -8 0
225 6 -93 0
-156 -243 349 0
-265 279 8 0
296 61 -339 0
-393 -330 66 0
-396 185 -59 0
260 175 -397 0
-177 -175 204 0
319 -410 288 0
-310 -384 423 0
75 401 433 0
207 6 397 0
-425 -405 -214 0
-360 -222 -269 0
251 287 -370 0
-420 -41 -370 0
242 264 -112 0
288 -315 -94 0
-341 -264 -223 0
46 -234 -324 0
20 -44 47 0
-366 -363 353 0
-323 -398 144 0
-389 56 438 0
-118 -411 -397 0
291 -163 -215 0
-299 -179 326 0
177 222 -105 0
-374 279 -148 0
-235 -40 -161 0
323 270 245 0
-385 -23 42 0
422 358 87 0
-192 325 -233 0
246 -151 359 0
-225 -203 36 0
159 -200 -61 0
-321 -62 296 0
332 -26 319 0
-241 370 -69 0
-9 342 -153 0
-281 -290 -428 0
72 -428 64 0
312 302 -44 0
351 130 384 0
383 329 64 0
-394 269 262 0
167 236 331 0
281 170 350 0
328 361 227 0
-427 54 321 0
210 136 -139 0
-168 -361 -349 0
354 -164 220 0
-364 -93 90 0
-140 -378 -89 0
-397 -320 -59 0
-166 -370 -282 0
-247 -130 117 0
139 -273 301 0
-418 226 354 0
156 428 131 0
-369 58 -22 0
291 -377 -92 0
116 -416 357 0
-380 329 20 0
42 108 -295 0
-349 -80 -314 0
-69 186 -255 0
-62 -184 448 0
-402 -9 267 0
294 -178 -257 0
94 400 -57 0
-129 291 -189 0
-278 44 -212 0
-433 22 317 0
431 -274 341 0
52 -298 -292 0
28 132 113 0
-137 -160 252 0
147 -274 -110 0
207 -410 443 0
39 238 -169 0
118 170 148 0
417 116 -150 0
374 -196 147 0
273 -3 101 0
-425 303 -418 0
237 -198 186 0
-120 -339 57 0
-208 447 -320 0
-351 -359 196 0
75 -314 275 0
-326 219 409 0
-42 -356 173 0
298 -137 22 0
7 385 172 0
38 139 326 0
218 320 -369 0
-239 -113 -25 0
-303 183 -339 0
413 162 216 0
281 234 25 0
-44 267 291 0
3 289 -28 0
-406 439 4 0
-80 -258 220 0
-40 25 155 0
-410 -18 94 0
-73 -81 -85 0
256 -205 335 0
100 -373 420 0
-121 43 305 0
254 -161 -49 0
121 -6 -385 0
209 114 -381 0
-69 -306 -319 0
56 -119 -143 0
116 150 -13 0
216 359 167 0
226 176 238 0
-332 346 -414 0
-14 -50 386 0
-310 -25 16 0
377 -238 435 0
237 357 385 0
18 -211 -360 0
132 -2 433 0
375 113 -304 0
-413 189 -324 0
398 355 -422 0
-312 -93 -150 0
-346 406 144 0
439 -366 -23 0
137 -339 -15 0
42 207 -318 0
383 294 -119 0
293 -115 170 0
48 -296 -174 0
-268 -257 176 0
211 13 -106 0
328 -347 253 0
-108 -65 -74 0
-228 431 -106 0
298 153 -293 0
-99 141 151 0
24 347 162 0
38 292 412 0
266 298 245 0
211 173 165 0
-57 189 130 0
-261 436 -207 0
-319 -423 -24 0
242 -60 85 0
9 -225 428 0
-215 -371 -148 0
421 264 36 0
272 85 370 0
-139 382 396 0
-356 -209 192 0
208 231 -54 0
-179 107 374 0
169 423 -290 0
-85 -224 -353 0
214 439 -196 0
239 -282 -190 0
74 -269 -321 0
44 -81 -357 0
265 -375 223 0
-246 216 -19 0
180 294 -157 0
-284 -95 -288 0
-387 -431 -439 0
356 -53 -218 0
375 -86 -355 0
-56 -349 -306 0
444 -109 -358 0
-366 42 -211 0
75 -52 318 0
80 261 399 0
307 -288 -321 0
-119 -225 -272 0
17 262 410 0
-15 100 -158 0
-203 3 -423 0
-137 244 -351 0
-210 -170 402 0
-8 -269 16 0
439 93 -160 0
387 386 389 0
-147 294 378 0
348 115 -205 0
386 178 188 0
408 256 307 0
-386 -241 -289 0
-75 324 -388 0
-112 -162 -365 0
-110 -299 333 0
359 233 -46 0
241 -361 -125 0
-347 -262 83 0
151 396 101 0
-422 284 -99 0
-297 -221 -220 0
78 399 129 0
-328 -393 365 0
-180 -294 -396 0
-397 353 67 0
348 -445 -26 0
-387 -227 -6 0
432 348 325 0
8 342 -446 0
-127 243 126 0
-276 -61 -322 0
-287 -63 -318 0
189 -259 -90 0
-400 399 -152 0
-27 -435 -63 0
54 -272 -271 0
-429 -136 12 0
164 -322 -193 0
-93 -423 134 0
57 -279 68 0
94 -146 -382 0
440 385 -362 0
179 -229 280 0
-143 66 -237 0
-400 -296 -337 0
138 324 -147 0
-262 -354 230 0
126 -301 -293 0
404 100 -421 0
83 323 369 0
-330 268 -393 0
33 -254 -413 0
216 263 181 0
389 5 361 0
237 -218 132 0
394 170 -168 0
-20 195 107 0
-131 -212 -278 0
-427 79 -425 0
368 -388 -427 0
28 -64 51 0
362 308 -257 0
87 304 127 0
-189 338 -283 0
-99 235 440 0
68 -32 292 0
272 299 141 0
386 -374 261 0
-291 379 202 0
347 438 -74 0
160 191 55 0
-387 174 -210 0
336 335 -239 0
-56 334 194 0
-216 65 -437 0
151 356 153 0
-431 -111 -217 0
-143 376 99 0
-110 297 -273 0
-127 -53 -27 0
350 301 225 0
233 -257 434 0
184 46 422 0
295 433 -339 0
-16 -58 -208 0
-310 -445 88 0
359 100 -351 0
321 -279 448 0
443 -390 -179 0
-251 435 194 0
-412 211 -331 0
-153 413 446 0
395 437 134 0
-288 351 -92 0
-173 362 -211 0
208 307 -214 0
-14 -358 34 0
226 -250 -281 0
429 -141 260 0
-31 -153 262 0
119 -379 -292 0
-115 407 71 0
-341 -49 404 0
-42 -345 -132 0
98 8 -324 0
87 398 262 0
137 83 337 0
272 358 -432 0
-416 -228 125 0
36 -169 214 0
-202 -272 -198 0
11 389 -340 0
446 24 342 0
-40 80 -250 0
237 -395 -99 0
-196 -4 396 0
-89 450 -262 0
287 -155 -310 0
414 116 -41 0
-324 -212 -171 0
150 365 398 0
-336 -4 130 0
-258 -410 228 0
246 36 82 0
232 334 -153 0
226 275 42 0
177 316 -133 0
255 227 334 0
38 -3 -307 0
-291 255 -272 0
121 69 -336 0
-245 74 -41 0
-378 -401 -111 0
-386 -20 -219 0
-41 -218 -83 0
222 -78 316 0
95 -316 -198 0
419 -258 446 0
18 364 368 0
433 162 -216 0
-375 -163 -315 0
416 68 408 0
414 321 53 0
425 154 41 0
-280 292 37 0
-386 154 -362 0
-363 346 -219 0
-275 -195 -11 0
41 -135 318 0
-70 323 -294 0
-29 -19 -376 0
382 304 -79 0
161 390 450 0
-424 -421 -405 0
-131 -9 317 0
-324 230 -398 0
404 -231 -405 0
380 -5 399 0
-214 -58 -255 0
-332 -400 174 0
368 -404 41 0
175 -416 397 0
138 154 365 0
-399 301 -339 0
-231 -48 -303 0
-23 -427 -271 0
-215 346 -431 0
-335 420 355 0
366 238 -9 0
224 -134 -26 0
-246 195 -153 0
354 -18 426 0
-2 91 -403 0
304 -223 -308 0
161 98 25 0
-329 -356 267 0
-9 15 -64 0
-364 72 -135 0
-24 -334 -45 0
170 385 184 0
-420 -18 -350 0
154 43 -374 0
-314 414 -386 0
-95 -174 215 0
156 269 178 0
-26 -420 281 0
182 187 -332 0
76 145 134 0
-230 66 257 0
329 -395 -24 0
136 -145 274 0
448 417 -249 0
-240 428 286 0
111 -29 72 0
209 336 437 0
20 333 -122 0
-258 104 27 0
-192 -380 344 0
-177 241 -27 0
-349 253 -340 0
-248 -319 -121 0
-177 -139 172 0
330 -432 144 0
-145 -221 98 0
204 117 -27 0
-126 401 -62 0
-400 76 -230 0
-61 200 75 0
-221 227 272 0
-275 -225 223 0
278 -238 -412 0
-58 90 151 0
-348 -303 -175 0
-327 -78 -312 0
79 -256 -152 0
378 -398 43 0
297 95 336 0
-31 148 407 0
-168 217 -322 0
109 -307 -231 0
-239 47 56 0
262 443 109 0
62 26 -252 0
224 -119 290 0
-149 -190 -132 0
18 211 -145 0
-122 388 68 0
-185 232 8 0
-149 -245 -75 0
34 -313 78 0
-206 -154 244 0
1 76 216 0
253 6 10 0
-326 -20 13 0
-211 66 -374 0
333 196 -21 0
-174 -26 -229 0
255 314 -333 0
16 -149 120 0
227 361 -305 0
433 -67 265 0
425 -205 373 0
164 -242 -347 0
-378 450 169 0
-356 140 -358 0
202 -218 -226 0
-8 -304 -178 0
-176 430 -19 0
342 -262 -339 0
332 131 18 0
265 30 -246 0
421 -86 51 0
21 203 153 0
-3 115 340 0
217 271 207 0
-298 -316 -273 0
201 -346 91 0
153 -198 -395 0
250 93 -431 0
254 -272 230 0
-196 333 65 0
173 -136 -259 0
-61 103 -271 0
-137 -202 -6 0
-430 -314 -41 0
185 -278 -107 0
167 -247 314 0
415 430 2 0
-370 109 -87 0
179 327 -213 0
-148 -188 -389 0
366 133 -323 0
-332 376 -230 0
-414 315 -250 0
160 325 343 0
380 12 109 0
443 36 281 0
155 -253 -363 0
219 -208 -37 0
-394 162 276 0
166 -97 -183 0
-398 156 -297 0
192 -304 -373 0
173 106 442 0
43 -286 -93 0
-163 338 40 0
-42 -193 263 0
70 437 -342 0
123 78 235 0
-219 -373 -358 0
30 -411 -225 0
-307 -37 -180 0
-293 128 44 0
-276 -119 300 0
222 -145 -23 0
-449 -289 -231 0
221 -93 370 0
201 -125 -313 0
-272 -34 -30 0
-387 -321 341 0
-440 286 -154 0
71 275 -61 0
421 220 143 0
-142 -61 -148 0
104 115 369 0
-261 235 -61 0
-68 165 -342 0
-26 139 389 0
380 263 425 0
-96 -9 53 0
408 179 -88 0
-111 366 3 0
-74 -255 -122 0
-434 441 9 0
-214 -148 -272 0
82 215 -283 0
121 334 -114 0
-327 -397 391 0
119 200 -323 0
332 17 171 0
225 -120 -378 0
95 -376 338 0
-34 384 25 0
416 -319 405 0
-241 -335 253 0
383 101 -421 0
-141 -89 254 0
-93 127 410 0
-386 127 -88 0
233 -56 427 0
-148 -195 -20 0
-347 -331 294 0
175 -24 432 0
75 -162 -304 0
-141 295 153 0
168 266 328 0
165 362 -20 0
35 206 62 0
87 -104 292 0
202 288 -249 0
357 439 139 0
-77 -56 7 0
101 -92 -420 0
205 5 335 0
-392 -114 -58 0
341 56 -105 0
137 359 -268 0
-49 230 -228 0
109 -135 -190 0
45 410 -443 0
35 -17 16 0
106 -402 -174 0
-28 313 -145 0
44 -73 -288 0
-121 -5 -341 0
-437 -308 370 0
-295 -243 213 0
-9 -423 -280 0
-395 -66 -153 0
98 102 -266 0
-95 350 191 0
-415 45 102 0
-265 317 248 0
259 -299 297 0
223 143 219 0
-287 -410 319 0
103 -215 -433 0
258 -367 59 0
-82 -156 -252 0
295 62 424 0
46 -266 -375 0
-184 -351 15 0
286 -252 76 0
-355 401 74 0
-430 109 -260 0
11 -275 -157 0
-182 -34 154 0
-292 -340 259 0
110 107 327 0
406 174 -285 0
-41 -353 9 0
-232 405 -248 0
9 217 415 0
-116 -141 347 0
-380 -221 156 0
-221 85 342 0
89 -364 134 0
329 -61 364 0
-265 -23 107 0
-240 -178 445 0
-7 -163 -138 0
-28 -90 -206 0
-148 292 250 0
-189 -251 70 0
313 210 400 0
382 -263 105 0
-212 -84 82 0
-308 180 216 0
-348 -40 153 0
-32 312 315 0
243 -333 115 0
446 19 374 0
-370 421 -10 0
269 264 299 0
-12 -272 303 0
-294 110 -179 0
74 233 228 0
65 344 -303 0
257 53 -193 0
365 -328 -149 0
349 314 -354 0
-322 -173 -62 0
324 36 -292 0
182 168 -179 0
308 -255 -382 0
249 114 -80 0
-21 397 165 0
-224 168 241 0
332 -172 -77 0
-444 301 -149 0
400 371 -342 0
115 175 -406 0
281 396 -330 0
-317 217 207 0
-341 241 202 0
94 21 -326 0
-334 245 392 0
59 176 -385 0
-59 294 -449 0
317 283 252 0
-62 -339 -38 0
374 97 74 0
426 -37 -16 0
25 -117 -439 0
368 -403 -190 0
-170 80 48 0
302 -34 290 0
-346 -147 -166 0
421 442 363 0
375 -397 442 0
38 359 -341 0
-367 201 -292 0
-175 137 377 0
-102 71 190 0
-261 -439 -433 0
219 -355 -120 0
274 -378 -253 0
-349 284 -165 0
-57 -392 -255 0
106 187 -201 0
-110 -169 -207 0
76 -239 195 0
-153 234 -267 0
397 -101 -111 0
140 -142 -225 0
101 112 272 0
134 -381 -426 0
33 -115 243 0
159 377 -404 0
-163 -248 100 0
236 -86 -93 0
-340 260 129 0
-405 135 -270 0
-172 176 -355 0
190 109 -168 0
50 435 95 0
-331 291 54 0
32 -269 -17 0
359 170 431 0
-222 342 -29 0
-420 -388 -180 0
114 156 438 0
441 49 -418 0
-144 129 112 0
60 -344 366 0
349 -164 -325 0
283 -370 -23 0
-16 -191 -399 0
-368 -93 -73 0
-8 -319 -81 0
9 -426 59 0
240 -274 79 0
-274 -407 -343 0
-94 188 -62 0
-210 -450 -354 0
448 -427 -148 0
-400 243 355 0
74 248 -256 0
121 -150 -283 0
-160 -364 -311 0
-316 -33 -300 0
260 -348 184 0
-313 -303 -36 0
249 -54 66 0
43 206 307 0
-153 299 35 0
77 238 -160 0
377 -141 -245 0
-212 -204 -185 0
194 -113 445 0
-373 -422 76 0
-293 -89 -165 0
-394 -24 -158 0
42 -187 -295 0
-257 137 -398 0
-367 -433 176 0
434 -404 -373 0
336 164 104 0
-106 -223 -149 0
-420 -59 347 0
-343 215 -7 0
339 -186 -278 0
-377 315 -341 0
112 143 393 0
-441 -178 89 0
303 339 185 0
-30 -153 360 0
58 -130 -115 0
227 127 -406 0
324 355 13 0
-80 -374 137 0
55 -313 -117 0
-218 -121 -18 0
-228 107 340 0
-132 78 102 0
-277 -43 -443 0
441 325 213 0
-157 308 -62 0
-369 -152 307 0
393 -52 -14 0
274 -436 147 0
65 25 238 0
-279 28 -14 0
202 -428 -299 0
225 -190 230 0
-275 -415 186 0
-40 -211 132 0
-379 -373 55 0
-88 -208 -56 0
-20 -361 362 0
81 -357 -384 0
182 443 -75 0
-198 -346 6 0
379 48 -31 0
-383 -375 -306 0
-154 263 356 0
208 -168 207 0
-359 -91 368 0
421 186 -296 0
191 -428 139 0
-214 311 357 0
-280 408 187 0
-65 -370 362 0
-95 202 104 0
-399 411 174 0
-192 -256 315 0
366 322 -108 0
-128 -325 440 0
407 228 196 0
-214 201 -412 0
45 173 320 0
-343 9 444 0
298 -71 -351 0
292 169 146 0
210 76 -35 0
381 -197 274 0
300 -251 431 0
374 146 370 0
-210 279 411 0
258 127 86 0
-113 -155 -297 0
261 426 -181 0
-204 -293 338 0
171 -434 -280 0
-228 192 220 0
-44 398 158 0
-393 -304 -420 0
-446 417 -36 0
-167 138 -40 0
-23 258 -404 0
297 212 -249 0
-349 399 309 0
-175 -11 263 0
145 -37 -114 0
241 155 -193 0
318 152 -156 0
337 255 186 0
-18 449 -75 0
-378 -281 -309 0
348 301 -381 0
-317 436 450 0
-373 310 33 0
-195 438 393 0
211 314 -447 0
-78 408 -74 0
337 -5 -407 0
251 353 202 0
-47 386 -140 0
-428 20 441 0
-71 157 377 0
135 -91 60 0
181 330 -312 0
-155 -209 260 0
-398 -72 -98 0
343 421 -102 0
413 356 -210 0
426 -430 216 0
7 124 246 0
162 321 -283 0
357 -340 -89 0
-449 399 -400 0
157 182 288 0
89 416 -387 0
-181 -343 -96 0
-213 205 99 0
51 -256 -23 0
-63 -236 248 0
13 -39 271 0
-154 -338 216 0
57 27 -198 0
-388 -170 119 0
-401 -397 -32 0
-131 379 -366 0
438 -40 264 0
-328 -206 -129 0
293 337 7 0
108 149 -15 0
-52 430 -116 0
-274 78 -61 0
-323 385 -339 0
297 408 382 0
203 -148 -389 0
-321 -338 439 0
215 -210 256 0
-63 -3 416 0
-34 -369 177 0
-346 112 227 0
431 189 -155 0
8 345 -273 0
-106 -273 -422 0
6 -346 247 0
437 -422 -30 0
-42 -246 -18 0
-130 294 341 0
-442 -339 71 0
297 226 373 0
-439 170 -255 0
-376 -375 -16 0
-132 -20 -395 0
-158 60 187 0
-101 198 -222 0
-275 -448 -362 0
-341 185 292 0
434 267 -95 0
43 449 138 0
-85 -277 415 0
-176 -435 95 0
-442 210 245 0
-340 -59 -227 0
109 -340 -119 0
-422 313 194 0
-197 -333 433 0
-64 441 -244 0
396 255 -180 0
-136 -86 282 0
-316 417 165 0
28 6 361 0
-247 426 -340 0
-97 265 447 0
-33 426 -267 0
275 240 -326 0
-290 -256 130 0
290 -286 117 0
143 -265 302 0
425 414 119 0
-40 150 136 0
177 -314 379 0
189 23 -170 0
442 225 -414 0
-18 426 112 0
113 -17 83 0
427 179 -247 0
-160 -245 -210 0
-350 32 278 0
78 171 -237 0
-73 149 -260 0
144 160 126 0
331 223 306 0
394 -85 264 0
95 272 -374 0
-435 162 386 0
237 189 285 0
-101 -274 217 0
-418 137 170 0
-191 441 -330 0
-422 -317 125 0
72 -159 391 0
221 161 -261 0
-418 153 424 0
-347 387 -66 0
157 233 163 0
288 -146 -228 0
215 276 -79 0
224 96 -142 0
292 -249 -418 0
-266 -347 54 0
415 -7 -74 0
268 -33 355 0
-323 -25 -445 0
-116 -293 -375 0
-383 244 348 0
235 -136 -75 0
397 -313 -292 0
-98 176 -7 0
-15 177 -61 0
266 54 -315 0
255 385 -360 0
6 -18 -365 0
-411 46 -158 0
425 251 -52 0
-278 -195 -203 0
94 22 -342 0
386 224 144 0
117 202 -246 0
-189 342 -41 0
262 -66 153 0
336 -70 170 0
35 -420 138 0
-31 61 -251 0
-315 -413 -226 0
-239 -75 175 0
219 -334 211 0
-339 190 393 0
341 -157 357 0
-102 61 399 0
418 -314 -37 0
99 417 -87 0
283 -40 -297 0
143 364 -171 0
-332 -270 122 0
-308 386 -237 0
334 390 366 0
-294 93 -329 0
-215 -261 365 0
299 257 225 0
-35 444 -95 0
46 295 39 0
135 -429 -6 0
7 -300 -22 0
447 57 -394 0
-273 58 -54 0
2 381 -228 0
353 -137 188 0
404 209 22 0
200 236 -111 0
16 -186 -354 0
275 262 -449 0
-380 -46 -383 0
-351 428 -390 0
280 301 -52 0
321 -151 260 0
281 -114 -47 0
98 -12 176 0
-410 205 227 0
103 192 214 0
334 182 411 0
-106 -148 -206 0
46 -123 -100 0
115 -16 -323 0
335 -243 -143 0
196 275 282 0
-61 -159 -182 0
350 -365 -271 0
227 415 -360 0
5 132 -406 0
-222 31 57 0
-170 -77 124 0
282 225 -238 0
136 -87 -301 0
-36 245 -442 0
-137 196 377 0
-257 -344 311 0
378 249 -169 0
-63 -264 71 0
-253 -332 267 0
346 276 107 0
-223 118 279 0
69 100 -216 0
-114 -437 122 0
95 -205 -237 0
-204 277 -245 0
-139 430 61 0
363 -221 17 0
-212 -55 -395 0
155 -245 -118 0
-221 399 45 0
88 -242 140 0
-262 -389 -38 0
430 267 120 0
-283 397 170 0
296 96 -217 0
-350 291 149 0
-429 -226 -441 0
-350 221 251 0
227 -350 -149 0
325 120 397 0
177 441 101 0
211 -329 -291 0
287 260 -293 0
-354 106 -347 0
157 86 163 0
-238 281 -105 0
157 -397 384 0
297 135 98 0
222 334 29 0
-319 -448 -91 0
-258 187 -304 0
439 -202 338 0
192 52 -425 0
-320 -22 -175 0
215 227 157 0
-299 214 -124 0
317 -368 82 0
360 55 -326 0
375 -48 345 0
373 -385 -99 0
-189 -121 -311 0
342 -10 209 0
211 335 158 0
196 401 -250 0
-421 -289 -235 0
440 -402 199 0
436 76 213 0
205 415 390 0
-182 -247 259 0
-111 38 404 0
102 -190 -270 0
286 -221 429 0
-284 -99 343 0
-80 171 -149 0
-270 391 2 0
-181 6 -275 0
227 149 93 0
-14 129 167 0
298 -170 76 0
235 -424 -234 0
330 165 268 0
275 282 239 0
-78 82 -262 0
-240 304 -35 0
217 254 185 0
167 -115 42 0
-354 -171 108 0
-207 -228 288 0
-138 -8 -219 0
-435 83 441 0
-108 -324 -11 0
176 81 -386 0
349 337 -307 0
-121 249 -366 0
39 313 -128 0
104 179 93 0
-291 148 -181 0
-316 -92 -216 0